\chapter{Mathematische Grundlagen}% \& softwaretechnische Betrachtungen}

Consize ist eine funktionale Programmiersprache, die nicht -- wie meist üblich -- auf dem Lambda-Kalkül, sondern auf einem Homomorphismus beruht, der Programme mit Funktionen und die Konkatenation von Programmen mit Funktionskomposition in Beziehung setzt

\section{Der konkatenative Formalismus in denotationeller Semantik}

Gegeben sei ein Vokabular $V=\{w_1, w_2, \dots\}$ mit einer \href{http://de.wikipedia.org/wiki/Menge\_(Mathematik)}{Menge} von Wör\-tern. Die Menge aller nur erdenklichen Sequenzen, die mit den Wörtern des Vokabulars $V$ gebildet werden können -- das beinhaltet sowohl die leere Sequenz als auch beliebige Verschachtlungen -- sei mit $S^V$ bezeichnet und werde mit Hilfe der \href{http://de.wikipedia.org/wiki/Kleenesche_und_positive_H\%C3\%BClle}{Kleeneschen Hülle} definiert; $S$ sei aus $V$ abgeleitet zu $S=\{[w_1],[w_2],\dots\}$:

$$S^V=S^{\ast}\cup(S^{\ast})^{\ast}\cup((S^{\ast})^{\ast})^{\ast}\cup\dots$$

Der Operator zur Konkatenation $\oplus: S^V\times S^V \rightarrow S^V$ konkateniere zwei Sequenzen
$[s_1,\dots,s_n]\oplus[s_1',\dots,s_m']=[s_1,\dots,s_n,s_1',\dots,s_m']$. $(S^V,\oplus,[\,])$ bildet einen \href{http://de.wikipedia.org/wiki/Monoid}{Monoid}: Die Operation der Konkatenation ist in sich geschlossen, die leere Sequenz ist das \href{http://de.wikipedia.org/wiki/Neutrales\_Element}{neutrale Element} der Konkatenation, und das \href{http://de.wikipedia.org/wiki/Assoziativgesetz}{Gesetz der Assoziativität} gilt.

Gegeben sei weiterhin die Menge der \href{http://de.wikipedia.org/wiki/Funktion\_(Mathematik)}{Funktionen} $F=\{f_1, f_2, \dots\}$, wobei für alle Funktionen $f\in F$ gilt: $f:S^V_{\bot}\rightarrow S^V_{\bot}$. Das Symbol $\bot$ markiert in der \href{http://de.wikipedia.org/wiki/Denotationelle\_Semantik}{denotationellen Semantik} den Fehlerfall, $S^V_{\bot}=S^V\cup\{\bot\}$. Es gilt: $f(\bot)=\bot$.

Der Operator zur \href{http://de.wikipedia.org/wiki/Komposition\_(Mathematik)}{Komposition zweier Funktionen}
$;:(S^V_{\bot}\rightarrow S^V_{\bot}) \times
(S^V_{\bot}\rightarrow S^V_{\bot}) \rightarrow
(S^V_{\bot}\rightarrow S^V_{\bot})$ definiere die Komposition zweier Funktionen 
$f:S^V_{\bot}\rightarrow S^V_{\bot}$
und 
$g:S^V_{\bot}\rightarrow S^V_{\bot}$
als $f;g: S^V_{\bot}\rightarrow S^V_{\bot}$, wobei gilt
$(f;g)(s)=g(f(s))$ für alle $s\in S^V_{\bot}$. Das neutrale Element der Funktionskomposition ist die \href{http://de.wikipedia.org/wiki/Identische\_Abbildung}{Identitätsfunktion} $id:S^V_{\bot}\rightarrow S^V_{\bot}$ mit $id(s)=s$ für alle $s\in S^V_{\bot}$. $(S^V_{\bot},;,id)$ bildet ebenfalls einen Monoid.

Zu den beiden Monoiden, der Konkatenation von Sequenzen und der Komposition von Funktionen, gesellen sich zwei weitere Funktionen, um die Bedeutung (Denotation) einer Sequenz als "`Programm"' zu definieren. Wir nennen eine solche Sequenz auch "`Quotierung"'.

Das Wörterbuch werde durch eine Funktion $D:V\rightarrow F$ gegeben: Jedes Wort ist eindeutig mit einer Funktion assoziiert. 
Die Funktion $self:S^V\rightarrow (S^V\rightarrow S^V)$ sei definiert als $self(s)(s')=[s]\oplus s'$, $s, s'\in S^V$.

Die Denotation $\ldenote s \rdenote$ einer Sequenz $s\in S^V$
liefert immer eine Sequenz verarbeitende Funktion zurück und
ist definiert über sämtliche Spielarten, die für die Sequenz $s$ denkbar sind: (1) wenn sie leer ist, (2) wenn sie ein einziges Wort enthält, (3) wenn sie eine einzige Sequenz enthält, und (4) wenn die Sequenz aus den vorigen Möglichkeiten zusammengesetzt ist.

\begin{enumerate}
\item[(1)] $\ldenote [\,] \rdenote = id$
\item[(2)] $\ldenote [ w] \rdenote = f$ für $w\in V$ und $f=D(w)$
\item[(3)] $\ldenote [ s] \rdenote = self(s)$ für $s\in S^V$.
\item[(4)] $\ldenote s_1\oplus s_2 \rdenote =
       \ldenote s_1 \rdenote ; \ldenote s_2 \rdenote$ für $s_1,s_2\in S^V$.
\end{enumerate}

Die vier Gleichungen betonen den \href{http://de.wikipedia.org/wiki/Homomorphismus}{Homomorphismus}: Die Konkatenation von Sequenzen findet ihr Abbild in der Komposition von Funktionen. Für \href{http://de.wikipedia.org/wiki/Turing-Vollst\%C3\%A4ndigkeit}{Turing-Vollständigkeit} genügt ein Homomorphismus allein nicht. Es fehlt etwas, das die \href{http://de.wikipedia.org/wiki/Selbstbez\%C3\%BCglichkeit}{Selbstbezüglichkeit} herstellt -- das entscheidende Merkmal turingvollständiger Systeme

Den notwendigen Selbstbezug stellt die zu $self$ inverse Funktion $self^{-1}$ her. Die Funktion sei
% implizit
definiert über den Zusammenhang

$$(self;self^{-1})(s) = \ldenote s \rdenote$$

% Aus der Gleichung ist in Auflösung der Funktionskomposition abzuleiten, dass $self^{-1}$ eine Funktion höherer Ordnung ist.

% $$self^{-1}(self(s)) = self^{-1}\ldenote [s] \rdenote = \ldenote s \rdenote$$

Das mit der Funktion $self^{-1}$ assoziierte Wort heiße \verb|call|. Statt diese Assoziation als Bestandteil des Wörterbuchs einzufordern, gelte mit \verb|call| $\notin V$ die fünfte "`Regel"':

\begin{enumerate}
\item[(5)] $\ldenote [$\verb|call|$] \rdenote = self^{-1}
\Rightarrow
\ldenote [s]\oplus[$\verb|call|$] \rdenote = \ldenote s \rdenote$
\end{enumerate}

Elementarer kann man eine Programmiersprache kaum mehr formalisieren. Es ist das Minimum dessen, was in Anlehnung an die \href{http://de.wikipedia.org/wiki/Kategorientheorie}{Kategorientheorie} den Formalismus zu einer \href{http://de.wikipedia.org/wiki/Kartesisch\_abgeschlossene\_Kategorie}{kartesisch abgeschlossen Kategorie} (\emph{cartesian closed category}) und damit turingvollständig macht.

Die Implikationen sind beachtlich: Der konkatenative Formalismus entledigt sich einer "`Bürde"' des Lambda-Kalküls: Variablen. Variablen sind in diesem System vollkommen überflüssig, was Begründungen über Consize-Programme erheblich vereinfacht und das gedankliche Mitführen von Umgebungsvariablen (wie in der Veranschaulichung des \href{http://de.wikipedia.org/wiki/Lambda-Kalk\%C3\%BCl}{Lambda-Kalküls} üblich) unnötig macht.

Das notwendige Arrangieren von Argumenten auf dem Stapel übernehmen so genannte Stack-Shuffler, die ihrerseits Funktionen sind und sich somit vollkommen einfügen in das Schema der Funktionskomposition.

Der konkatenative Formalismus ist -- ähnlich dem Lambda-Kalkül -- in dieser extremen Reduktion kaum einsatztauglich für praktische Programmierzwecke. Entscheidend ist die Einführung benamter Abstraktionen. Namen sind wichtige "`Krücken"' in der Begrenzung des menschlichen Intellekts sich anonyme Abstraktionen praktisch kaum merken zu können.

\section{Der Bezug zur operationalen Semantik, der Consize-VM}

Der konkatenative Formalismus und die \href{http://de.wikipedia.org/wiki/Operationale\_Semantik}{operationale Semantik} scheinen sich auf den ersten Blick fremd zu sein. Tatsächlich ist die operationale Semantik dem konkatenativen Formalismus sehr treu.

Wörter, Funktionen und Sequenzen (in Consize durch Stapel implementiert) sind leicht in Deckung gebracht. Die Funktion von Mappings (in anderen Sprachen auch als Hashmaps, assoziative Arrays oder Dictionaries bezeichnet) kann durch Stapel emuliert werden. Mappings sind für ihren Einsatzzweck jedoch deutlich effizienter als es Stapel sind.

Die folgenden Betrachtungen beziehen sich auf die operationale Semantik, so wie sie in Kap.~\ref{Sec:Continuations} durch das Wort \verb|stepcc| definiert ist. Dabei gehen wir ausführlich auf die drei Fallunterscheidungen bei der Beschreibung von \verb|stepcc| ein (S.~\pageref{description.stepcc} ff.).

\smallskip\noindent{\bf Zum ersten Punkt in der operationalen Semantik}\marginpar{\texttt{itm} ist ein Wort}
Die scheinbare Erweiterung, das globale Wörterbuch nicht nur auf die Assoziation mit Funktionen zu beschränken und auf Quotierungen auszudehnen, begründet sich in den Gleichungen (2) und (4). Statt neue Funktionen über die Funktionskomposition zu bilden und im Wörterbuch mit Wörtern zu assoziieren, stellt Gleichung (4) die Option in den Raum, eine Quotierung im Wörterbuch einzutragen. Semantisch ändert sich dadurch nichts, solange jede Quotierung so weit auf Einzelwörter "`dekonkateniert"' und durch assoziierte Quotierungen aufgelöst wird, bis eine Funktion im Wörterbuch die Ausführung der Funktion laut Gleichung (2) einfordert. \verb|stepcc| setzt diese Option konsequent um.

Diese Option hat mehrere, entscheidende Vorteile: Erstens sind auf diese Weise zwanglos benamte Abstraktionen eingeführt. Unbenamte Quotierungen werden als "`anonyme Abstraktionen"' bezeichnet, benamte, sprich über das Wörterbuch assoziierte Quotierungen als "`benamte Abstraktionen"'.

Zweitens fehlt Funktionen eine sie identifizierende Repräsentation; alle Funktionen werden durch \verb|<fct>| repräsentiert. Würde Consize ausschließlich Wörter mit Funktionen assoziieren, so wären die Repräsentationen der Funktionsabstraktionen aussagelos. Dagegen sprechen die in Quotierungen enthaltenen Wörter Klartext; sie sind identisch mit dem Programmtext bei der Programmierung. Damit ist die Reflektion von Abstraktionen in Consize sehr einfach.

Das hat drittens zur Folge, dass man den Callstack bzw. Quotierungen nicht nur einfach reflektieren, sondern ebenso einfach manipulieren kann. Davon macht \verb|call/cc| Gebrauch, indem es die auf dem Datastack liegende Quotierung zum Programm macht und die "`übrige"' Continuation frei gibt zur beliebigen Manipulation. Streng genommen kann mit \verb|call/cc| der konkatenative Formalismus ausgehebelt werden, da eine uneingeschränkte Manipulation der rechnerischen Zukunft eines Programms möglich ist. Übt man ein wenig Programmierdisziplin und nutzt \verb|call/cc| im Sinne einer \emph{delimited continuation}, so ist das unkritisch und wieder im Einklang mit dem konkatenativen Formalismus. So ist denn auch die Realisierung von \verb|call| (Gleichung (5)) mittels \verb|call/cc| unproblematisch wie auch das Parsen von Klammern zur Laufzeit.

Anbei bemerkt zeigt die Diskussion einen interessanten Zusammenhang auf: Delimited Continuations sind das Laufzeitäquivalent einer Vorverarbeitung einer Quotierung vor ihrem Aufruf mit \verb|call|.

Viertens kann ein konkatenatives Programmiersystem auch gänzlich anders, nämlich über ein Rewriting System mit Pattern Matching und Pattern Instantiation implementiert werden,
% \cite{denkspuren:2009-09-17}
was insbesondere das Stack-Shuffling so gut wie überflüssig macht.

Das Meta-Wort \verb|read-word| ist ein pragmatisches Feature, um auch unbekannte, nicht im Wörterbuch aufgeführte Wörter in Anwendung von Gleichung (2) grundsätzlich mit einer Funktion zu assoziieren. 

\smallskip\noindent{\bf Zum zweiten Punkt}\marginpar{\texttt{itm} ist ein Mapping}
Ähnlich zu \verb|read-word| ist \verb|read-mapping| ein Feature, um Mappings -- die ja auch durch Stapel umgesetzt werden könnten -- gemäß Gleichung (3) zu behandeln oder ihnen, sofern ein Mapping etwas anderes darstellen soll, eine Sonderbehandlung zukommen zu lassen.

\smallskip\noindent{\bf Zum dritten Punkt}\marginpar{\texttt{itm} ist weder Wort noch Mapping}
Wenn \verb|itm| weder ein Wort noch ein Mapping ist, dann muss es ein Stapel, eine Funktion oder "`nil"' sein. Gleichung (3) beschreibt die Behandlung eines Stapels. Funktionen sind entsprechend der dargelegten Argumentation wie Quotierungen, d.h. ebenfalls wie Stapel zu behandeln. Da "`nil"' in Consize nur im Kontext von Stapeln eine Funktion hat, ist auch hier Gleichung (3) schlüssig angewendet.

\smallskip\noindent Die Consize-Implementierung ist ein zu Lehrzwecken geeignetes Beispiel, welche Design-Optionen ein Formalismus erlaubt, um ihn als Virtuelle Maschine zu realisieren. Die Funktion \verb|stepcc| beansprucht keine 20 Zeilen Code in ihrer Implementierung. 


%\section{Rekursion}
%% Benamte und unbenamte Rekursion
%% Wechselseitige Rekursion
%% Tail Recursion

%\section{Interaktion}

%\section{Komplexität}
%% Algorithmische Komplexität
%% Verhaltenskomplexität

%\section{Das Storytelling in der Softwaretechnik}
% "Namen sind Schall und Rauch" -- was aus der Sicht des Computers
% stimmt, und aus der Sicht eines Menschen falscher nicht sein
% könnte.
% Menschen betreiben ihr Engineering mit Worten und mit Geschichten.
% Die Gefahr: Die Stories sind nicht notwendigerweise konsistent. Sie
% haben Brüche, bedienen sich Metaphern etc. Die Ableitung einer Story
% aus den Vorgängen im Rechner mag noch nachvollziehbar und begründet
% sein. Die Rückübertragung der Story auf die Abläufe im Rechner mag
% die tatsächlichen Vorgänge vollkommen verfehlen.
% Ein Computersystem arbeitet mit Manipulationen von Symbolen, mit
% syntaktischen Operationen, denen jegliche Semantik und Metaphorik fremd
% ist.
% Löscht 'clear' den Datastack? Nein, nicht wirklich. Aber das ist
% die Story, die uns den Vorgang in seiner Semantik erinnerlich
% macht. Vielmehr noch: Das Wort und die Story übersetzt die internen
% Abäufe im Rechner in eine für uns beherrschbare Welt der operativen
% Zusammenhänge.
% Daraus begründet sich auch immer wieder, warum wir bei der Erfassung
% der Anforderungen an ein SW-System, stets Wechsel der
% Beschreibungsformen suchen sollten unter einem zunehmenden Grad der
% Formalisierung. Menschen können dann ihre Semantiken aus den
% operationalisierten Abläufen der Maschine ableiten und abgleichen.
% Software Engineering ist darum im besten Sinne Sprach-Engineering und
% ein Story-Telling.

%\section{Software Architektur: Verfeinerung und Abstraktion}

%\section{Modellbildung als Unschärfe}

%\section{Softwaretest}


